$\vdash$ $\forall$$A$:Type, $r$:($A$$\rightarrow$$A$$\rightarrow\mathbb{P}$). WellFnd\{i\}($A$;$x$,$y$.$r$($x$,$y$)) $\in$ $\mathbb{P}$'